HW#3 --- last modified January 29 2019 04:28:20.

Solution set.

Due date: Nov 3

Files to be submitted:
  Hw3.zip

Purpose: To gain familiarity with CSP heuristics and KB Agents

Related Course Outcomes:

The main course outcomes covered by this assignment are:

LO2 -- By code or by hand translate sentences in logic to conjunctive normal form (CNF).

LO3 -- By code or by hand find proofs by using resolution.

LO7 -- Students should be able to explain the advantages and disadvantages of forward checking in constraint satisfaction.

Specification:

This homework consists of a written component and a coding component. Files for both components should be submitted in your Hw3.zip file along with a readme.txt with any additional instructions, a list of your team mates and their IDs. For the written part, please do the following problems and submit them in a file Hw3.pdf within the Hw3.zip file

1. Consider the problem of getting a BSCS at SJSU. Simplify the prerequisite graph of CS courses by only consider deep course sequences (i.e., CS157A, CS157B; ; etc) which have CS146 only as a prerequisite for the first course. Treat all these sequences as the same sequence CSDeepA and CSDeepB. Write down the the task of just scheduling your CS courses as a CSP. You should have sufficient constraints so that a solution would mean that you have satisfied all undergrad CS requirements (you can ignore general ed and other requirements). Your domains should be the possible semesters to start a course or DNT if the course was not taken. For example, 1 means you start the course the first semester, 2 the second, etc. Let 8 be the highest semester number and assume you can take at most 5 courses a semester.
2. Let CS46B be the variable corresponding to the class CS46B. If we use the degree heuristic to choose the first variable in backtracking search to solve our CSP and if we break ties by picking the smaller numbered course, what is the variable X that would be considered in backtracking search in your CSP and what course does it correspond to? What would be the result of the REVISE(csp, X,CS46B)?
3. Suppose we choose CS49C to be taken in the first semester. Show all of the domains for each course after doing an arc consistency check (you only need to list the ones that change), in doing the check carefully trace the AC3 algorithm. In terms of works you did, how did this compare to the REVISE operation of the previous problem.,
4. From this updated CSP, using the MINIMUM REMAINING VALUE heuristic, give the variable to consider next. Break ties by choosing the course of smaller number.
5. Using the variable from the last step, determine the value for it using the LEAST-CONSTRAINING-VARIABLE heuristic breaking ties by picking the earliest possible semester.
6. This next problem is unconnected with the five previous. Come up with a logical formula which expresses `P_{3,3}`, there is a pit in square `(3,3)`, in terms of the variables (more than one) `B_{x,y}` expressing there is a breeze in square (x,y). Convert this formula to CNF by hand by first doing biconditional elimination, then implication elimination, then using distributivity. Check your work by downloading the software from Russell and Norvig (the book's code requires Python3), launching the Python interpreter, typing from logic import * then doing to_cnf("your original formula"). Obviously, replace "your original formula" with the formula you had before converting to CNF. Have the transcript of your interaction with Python as part of your solution.

For the coding part of the assignment, I want you to port the following two PHP programs to Python. I am not expecting you know PHP to do this, most of the constructs in the two languages are pretty close, so should be easy to translate, look up only what you need to get the rest. Try to do as close to a function by function port as possible.

This first program generates random CNF formulas according in the format used by satcompetition.org. Call your port cnf_generator.py

<?php
if (count($argv) < 4) {
    echo <<< 'EOD'
Random CNF generator
====================
This program is run from the command line with arguments:
php cnf_generator.php $num_variables $num_clauses $max_width
Its output format matches that used by satcompetition.org
EOD;
    exit();
}
list(,$num_variables, $num_clauses, $max_width,) = $argv;
echo <<< EOD
c
c Random CNF in satcompetition.org format created by cnf_generator.php
c
p cnf $num_variables $num_clauses

EOD;
for ($i = 0; $i <= $num_clauses; $i++) {
    $out = [];
    for ($j = 1; $j <= $max_width; $j++) {
        $k = mt_rand(1, $num_variables);
        $out[$k] = mt_rand(0, 1) ? $k : -$k;
    }
    echo implode(" ", $out) ." 0\n";
}

The second program is an implementation of the DPLL algorithm in PHP that takes as input a filename of a file containing clauses in the satcompetition.org format and then outputs the steps of the DPLL solver. When you port this program you don't have to exactly match the output of print_r and var_dump statements used to print arrays and variables, you can just use the analogous python operation. Call your port sat_solver.py.

<?php
if (count($argv) < 2 ) {
    echo <<< 'EOD'
sat_solver is a program used to read in a set of clauses in satcompetition.org
and output whether it is satisfiable or not. It is run from the command line
using the syntax:
php sat_solver.php filename
EOD;
}
$lines = file($argv[1]);
$clauses = [];
foreach ($lines as $line) {
    $line = trim($line);
    if ($line[0] == 'c' || $line[0] == 'p') {
        continue;
    }
    $pre_clause = preg_split("/\s+/", $line);
    $clause = [];
    foreach ($pre_clause as $pre_literal) {
        $literal = intval($pre_literal);
        if ($literal != 0) {
            $clause[] = $literal;
        }
    }
    if (!empty($clause)) {
        $clauses[] = $clause;
    }
}
echo "Clauses";
print_r($clauses);
var_dump(dpllSat($clauses));

function dpllSat($clauses)
{
   $symbols = getSymbolsClauses($clauses);
   return dpll($clauses, $symbols, []);
}
function dpll($clauses, $symbols, $assignment)
{
echo "Symbols\n";
print_r($symbols);
echo "Assignment\n";
print_r($assignment);
    if (checkAllClausesTrue($clauses, $assignment)) {
        return $assignment;
    }
    if (checkForFalseClause($clauses, $symbols, $assignment)) {
        return false;
    }
    $literal = findPureSymbol($symbols);
    if ($literal) {
        return dpll($clauses, array_diff($symbols, [$literal, -$literal]),
            $assignment + [$literal => 1, -$literal => -1]);
    }
    $literal = findUnitClause($clauses, $assignment);
    if ($literal) {
        return dpll($clauses, array_diff($symbols, [$literal, -$literal]),
            $assignment + [$literal => 1, -$literal => -1]);
    }
    $literal = choose($symbols);
    $symbols = array_diff($symbols, [$literal, -$literal]);
    $sat_assignment = dpll($clauses, $symbols,
            $assignment + [$literal => 1, -$literal => -1]);
    if ($sat_assignment === false) {
        $sat_assignment = dpll($clauses, $symbols, 
            $assignment + [$literal => -1, -$literal => 1]);
    }
    return $sat_assignment;
}
function getSymbolsClauses($clauses)
{
    $symbols = [];
    foreach($clauses as $clause) {
        foreach ($clause as $literal) {
            $symbols[$literal] = $literal;
        }
    }
    return array_values($symbols);
}
function checkAllClausesTrue($clauses, $assignment)
{
    foreach($clauses as $clause) {
        $value = false;
        foreach ($clause as $literal) {
            if (isset($assignment[$literal]) && $assignment[$literal] > 0) {
                $value = true;
                break;
            }
        }
        if (!$value) {
            return false;
        }
    }
    return true;
}
function checkForFalseClause($clauses, $symbols, $assignment)
{
    foreach($clauses as $clause) {
        $value = true;
        foreach ($clause as $literal) {
            if (in_array($literal, $symbols)) {
                $value = false;
                break;
            }
            if ($assignment[$literal] > 0) {
                $value = false;
                break;
            }
        }
        if ($value) {
            return true;
        }
    }
    return false;
}
function findPureSymbol($symbols)
{
    foreach ($symbols as $literal) {
        if (!in_array(-$literal, $symbols)) {
            return $literal;
        }
    }
    return false;
}
function findUnitClause($clauses, $assignment)
{
    $assigned_literals = array_keys($assignment);
    foreach ($clauses as $clause) {
        $unassigned = array_diff($clause, $assigned_literals);
        if (count($unassigned) == 1) {
            $already_true = false;
            foreach ($clause as $literal) {
                if(isset($assignment[$literal]) && $assignment[$literal] > 0) {
                    $already_true = true;
                    break;
                }
            }
            if (!$already_true) {
                return array_pop($unassigned);
            }
        }
    }
    return false;
}
function choose($symbols)
{
    return array_pop($symbols);
}

Once you have done your ports, generate three cnf's using the first program. Make sure at least one of these is unsatisfiable. By hand, find resolution proofs or satisfying assignment for each. Run your DPLL solver on the three examples and verify whether it produces the same output. Show your work and transcripts of running your solver in Hw3.pdf.

Point Breakdown